#!/bin/sh
echo "Создаю проект"
mkdir -p database tasks tasks/test

cat > script.ys <<EOF
read -sv sumn.v
prep -top sumn

write_ilang database/design.il
EOF

cat > sumn.v <<EOF
module sumn
  (
   // input wire
   input wire [7:0]   m_in, n_in,
   // output wire
   output wire [15:0] s_out
   );

   assign s_out = (n_in>=m_in)
   &(n_in>0)
   &(m_in>0)
   ?(m_in + n_in) 
   * (n_in - m_in + 1) 
   / 2
   :0;   
endmodule // calculator
EOF

cat > sumn_sim_tb.v <<EOF
// Example usage:
// iverilog -s sumn_sim_tb -o sumn_sim_tb sumn_sim_tb.v sumn.v && vvp -N bitcnt_tb

module sumn_sim_tb;
  reg  [ 7:0] mdin;
  reg  [ 7:0] ndin;
  wire [15:0] sdout;

  sumn uut (
    .m_in  (mdin ),
    .n_in  (ndin ),
    .s_out (sdout)
  );

  task test;
    input [ 7:0] mi;
    input [ 7:0] ni;
    input [15:0] si;
    begin
      mdin = mi;
      ndin = ni;
      #20;
      if (si === sdout) begin
        \$display("OK mi=%d ni=%d do(ref)=do(uut)=%d si=%d", mi, ni, sdout,si);
      end else begin
        \$display("ERROR mi=%d ni=%d do(ref)=do(uut)=%d si=%d", mi, ni, sdout,si);
        \$stop;
      end
      #20;
    end
  endtask

\`ifdef RAND   
   reg [ 7:0]  N,M;
   reg [15:0]  result;
   
   integer     seed =77;
  
   initial begin
      // Проверяем граничные наборы данных
      test(0,0,0);
      test(0,1,0);
      test(0,36,0);
      test(36,0,0);      
      test(1,0,0);
      test(1,1,1);
      test(0,2,0);
      test(1,2,3);
      test(1,3,6);
      test(13,80,3162);
      test(80,13,0);
      test(1,255,32640);
      test(7,7,7);
      // Здесь присвоим случайные значения
      repeat(127) begin
	 N = \$random(seed);
	 M = \$random(seed);
	 result = (N>0)&(M>0)&(N>=M)?((N+M)*(N-M+1))/2:0;
	 test(M,N, result);
      end
      \$display("PASS tests");
      \$finish;
   end
\`else   
 initial begin
   test(0,0,0);
   test(0,1,0);
   test(1,0,0);
   test(1,1,1);
   test(0,2,0);
   test(1,2,3);
   test(1,3,6);
   test(13,80,3162);
   test(80,13,0);
   test(1,255,32640);
   test(7,7,7);
   test(11,11,11);
   test(21,21,21);
   test(31,31,31);
   test(41,41,41);
   test(51,51,51);
   test(55,55,55);
   test(127,127,127);
   test(254,254,254);
   test(255,255,255);
   test(256,256,0);
   \$display("PASS tests");
   \$finish;
 end
\`endif

   initial begin
      \$dumpfile("out.vcd");
      \$dumpvars(0, sumn_sim_tb);
   end

endmodule
EOF

cat > config.mcy <<EOF
[options]
size 21
tags COVERED UNCOVERED NOCHANGE EQGAP FMONLY

[script]
read -sv sumn.v
prep -top sumn

[files]
sumn.v

[logic]
use_formal = True

sim_okay = result("test_sumn_sim") == "PASS"
eq_okay = result("test_sumn_eq") == "PASS"

if sim_okay and use_formal:
    sim_okay = (result("test_sumn_fm") == "PASS")
    if not sim_okay:
        tag("FMONLY")

if sim_okay and not eq_okay:
    tag("UNCOVERED")
elif not sim_okay and not eq_okay:
    tag("COVERED")
elif sim_okay and eq_okay:
    tag("NOCHANGE")
elif not sim_okay and eq_okay:
    tag("EQGAP")
else:
    assert 0

[report]
if tags("EQGAP"):
    print("Found %d mutations exposing a formal gap!" % tags("EQGAP"))
if tags("COVERED")+tags("UNCOVERED"):
    print("Coverage: %.2f%%" % (100.0*tags("COVERED")/(tags("COVERED")+tags("UNCOVERED"))))

[test test_sumn_sim]
expect PASS FAIL
run bash \$PRJDIR/test_sumn_sim.sh

[test test_sumn_eq]
expect PASS FAIL
run bash \$PRJDIR/test_sumn_eq.sh

[test test_sumn_fm]
expect PASS FAIL
run bash \$PRJDIR/test_sumn_fm.sh

EOF
cat > test_sumn_sim.sh <<EOF
#!/bin/bash

exec 2>&1
set -ex

bash \$SCRIPTS/create_mutated.sh

iverilog -o sim -D RAND ../../sumn_sim_tb.v mutated.v
vvp -n sim > sim.out

if grep PASS sim.out && ! grep ERROR sim.out; then
        echo "1 PASS" > output.txt
elif ! grep PASS sim.out && grep ERROR sim.out; then
        echo "1 FAIL" > output.txt
else
        echo "1 ERROR" > output.txt
fi

exit 0
EOF

cat > test_sumn_eq.sh <<EOF
#!/bin/bash

exec 2>&1
set -ex

bash \$SCRIPTS/create_mutated.sh -c -o mutated.il

ln -fs ../../test_sumn_eq.sv ../../test_sumn_eq.sby .

sby -f test_sumn_eq.sby
gawk "{ print 1, \\\$1; }" test_sumn_eq/status >> output.txt

exit 0
EOF

cat > test_sumn_eq.sv <<EOF
module miter (
        input [ 7:0] ref_mdin,
        input [ 7:0] uut_mdin,
        input [ 7:0] ref_ndin,
        input [ 7:0] uut_ndin,

        input [15:0] result_din
);
        wire [15:0] ref_sdout;
        wire [15:0] uut_sdout;

        sumn ref (
                .mutsel     (1'b 0),
                .m_in(ref_mdin),  // (ref_din_data),
                .n_in(ref_ndin),  // (din_func),
                .s_out(ref_sdout) // (ref_dout_data)
        );

        sumn uut (
                .mutsel    (1'b 1),
                .m_in(uut_mdin),  // (uut_din_data),
                .n_in(uut_ndin),  // (din_func),
                .s_out(uut_sdout) // (uut_dout_data)
        );
   always @* begin
      assume ((ref_mdin == uut_mdin)
	&& (ref_ndin == uut_ndin));
      assert (ref_sdout == uut_sdout);      
   end

endmodule
EOF

cat > test_sumn_eq.sby <<EOF
[options]
mode bmc
depth 1
expect pass,fail

[engines]
smtbmc yices

[script]
read_verilog -sv test_sumn_eq.sv
read_ilang mutated.il
prep -top miter
fmcombine miter ref uut
flatten
opt -fast

[files]
test_sumn_eq.sv
mutated.il
EOF

cat > test_sumn_fm.sv <<EOF
module test_sumn_fm_tb (
    input [ 7:0] mi,
    input [ 7:0] ni,
    output [ 15:0] out
);

    sumn u_sumn_mutated (
        .m_in (mi),
        .n_in (ni),
        .s_out(out)
    );

    always @* begin
        assume(mi > 0);
        assume(ni > 0);
        assume(ni >= mi);
        assert(out >= 1);
    end

endmodule
EOF

cat > test_sumn_fm.sby <<EOF
[options]
mode bmc
depth 1
expect pass,fail

[engines]
smtbmc boolector

[script]
read_verilog -sv test_sumn_fm.sv
read_ilang mutated.il
prep -top test_sumn_fm_tb
flatten
opt -fast

[files]
test_sumn_fm.sv
mutated.il

EOF

cat > test_sumn_fm.sh <<EOF
#!/bin/bash

exec 2>&1
set -ex

## create the mutated design

bash \$SCRIPTS/create_mutated.sh -o mutated.il

## run formal property check
ln -s ../../test_sumn_fm.sv ../../test_sumn_fm.sby .
sby -f test_sumn_fm.sby

## obtain result
gawk "{ print 1, \\\$1; }" test_sumn_fm/status >> output.txt

exit 0

EOF

cat > Makefile <<EOF
.DEFAULT_GOAL := help
NAME=Sumn
.PHONY: help
help:
	@echo ""
	@echo "Добро пожаловать в \$(NAME)!"
	@echo ""
	@echo "  Для работы установите"
	@echo " export SCRIPTS=/usr/local/share/mcy/scripts"
	@echo ""
	@echo "Используйте 'make <target>' где <target> одно из:"
	@echo ""
	@echo "  all      создаёт рабочие файлы проекта"
	@echo "  sim      тестирует настройки для testbench"
	@echo "  eq       тестирует настройки для eq"
	@echo ""
	@echo "  tb       прогон testbench"
	@echo "  clean_tb очмстит артефакты testbench: a.out, out.vcd"
	@echo ""
	@echo "  sim_rand установит RAND в testbench"
	@echo "           устанавлено по умолчанию"
	@echo "  sim_hand установит HAND в testbench"
	@echo ""
	@echo "  init     создаст новую базу данных"
	@echo "           эквивалентно mcy init"
	@echo "  mcy_run  выполнит mcy run"
	@echo "           эквивалентно mcy run"
	@echo "  purge    удалит текущую базу данных"
	@echo "           эквивалентно mcy purge"
	@echo ""
	@echo "  clean    удалит текущие рабочие файлы"
	@echo ""
	@echo "  Go forth and make something great!)))"
	@echo ""

SUBMAKE := \$(MAKE) --no-print-directory -C

.PHONY: all init purge mcy_run clean clean_tb

#all: sim eq
all: sumn
	sh \$^

.PHONY: sim 

sim: script.ys run_sim

script.ys: sumn
	sh \$^

run_sim: script.ys
	yosys \$^
	\$(SUBMAKE) tasks/test sim

.PHONY: eq

eq:
	\$(SUBMAKE) tasks/test eq

.PHONY: sim_hand

sim_hand: sim_hand.sh
sim_hand.sh: test_sumn_sim.sh
	cat \$^ | gawk '{ print gensub(/-D RAND/,"",1)}' > \$@
	mv \$@ \$^

STR_RAND='{ print gensub(/-o sim/,\$\$2" "\$\$3 " -D RAND",1)}'
.PHONY: sim_rand
sim_rand: test_sumn_sim.sh
	cat \$^ | gawk \$(STR_RAND) > \$@.sh
	mv \$@.sh \$^

.PHONY: tb

tb: a.out out.vcd wave
a.out: sumn.v sumn_sim_tb.v
	iverilog -D RAND \$^ -o \$@
out.vcd: a.out
	vvp \$^ -o \$@
wave: out.vcd
	gtkwave \$^

purge:
	mcy purge

init:
	mcy init

mcy_run:
	mcy run

clean:
	rm config.mcy 
	rm *.ys *.v *.sv *.sh *.sby *.out *.vcd

clean_tb:
	rm *.out *.vcd

EOF

cat > tasks/test/Makefile <<EOF
.PHONY: sim eq

sim: input.txt run_scripts_sim
input.txt: 
	echo "1 mutate -mode none" > \$@
run_scripts_sim:
	bash ../../test_sumn_sim.sh

eq: run_ln run_scripts_eq
	
run_ln:
	ln -s ../../test_sumn_eq.sv ../../test_sumn_eq.sby .

run_scripts_eq:
	bash ../../test_sumn_eq.sh
	sby -f test_sumn_eq.sby
EOF

echo "Проект создан! Тестируйте его согласно инструкциям в README"
